\begin{tabbing}
$\forall$\=$P$, $Q$:(ES\{i\}$\rightarrow\mathbb{P}$\{i'\}), $X$:es{-}real\{i:l\}(${\it es}$.$P$(${\it es}$)), $Y$:es{-}real\{i:l\}(${\it es}$.$Q$(${\it es}$)),\+
\\[0ex]$p$:R{-}compat\=\{i:l\}\+
\\[0ex](($X$.1); ($Y$.1)).
\-\-\\[0ex]es{-}real{-}and\{i:l\}($P$; $Q$; $X$; $Y$; $p$) $\in$ es{-}real\{i:l\}(${\it es}$.($P$(${\it es}$) \& $Q$(${\it es}$)))
\end{tabbing}